Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in recent competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this paper, we have developed VEL, a formally verified EL++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Our results justify further research in automatic translation of sentences for symmetry reduction.

Artificial intelligence (AI) has emerged as a transformative and versatile tool, breaking new frontiers across scientific domains. Among its most promising applications, AI research is blossoming in concrete science and engineering, where it has offered new insights towards mixture design optimization and service life prediction of cementitious systems. This chapter aims to uncover the main research interests and knowledge structure of the existing literature on AI for concrete materials. To begin with, a total of 389 journal articles published from 1990 to 2020 were retrieved from the Web of Science. Scientometric tools such as keyword co-occurrence analysis and documentation co-citation analysis were adopted to quantify features and characteristics of the research field. The findings bring to light pressing questions in data-driven concrete research and suggest future opportunities for the concrete community to fully utilize the capabilities of AI techniques.

Concrete domains, especially those that allow to compare features with numeric values, have long been recognized as a very desirable extension of description logics (DLs), and significant efforts have been invested into adding them to usual DLs while keeping the complexity of reasoning in check. For expressive DLs and in the presence of general TBoxes, for standard reasoning tasks like consistency, the most general decidability results are for the so-called $\omega$-admissible domains, which are required to be dense. Supporting non-dense domains for features that range over integers or natural numbers remained largely open, despite often being singled out as a highly desirable extension. The decidability of some extensions of $\mathcal{ALC}$ with non-dense domains has been shown, but existing results rely on powerful machinery that does not allow to infer any elementary bounds on the complexity of the problem. In this paper, we study an extension of $\mathcal{ALC}$ with a rich integer domain that allows for comparisons (between features, and between features and constants coded in unary), and prove that consistency can be solved using automata-theoretic techniques in single exponential time, and thus has no higher worst-case complexity than standard $\mathcal{ALC}$. Our upper bounds apply to some extensions of DLs with concrete domains known from the literature, support general TBoxes, and allow for comparing values along paths of ordinary (not necessarily functional) roles.

The aim of this work is to provide a family of qualitative theories for spatial change in general, and for motion of spatial scenes in particular. To achieve this, we consider a spatio-temporalisation MTALC(Dx), of the well-known ALC(D) family of Description Logics (DLs) with a concrete domain: the MTALC(Dx) concepts are interpreted over infinite k-ary Sigma-trees, with the nodes standing for time points, and Sigma including, additionally to its uses in classical k-ary Sigma-trees, the description of the snapshot of an n-object spatial scene of interest; the roles split into m+n immediate-successor (accessibility) relations, which are serial, irreflexive and antisymmetric, and of which m are general, not necessarily functional, the other n functional; the concrete domain Dx is generated by an RCC8-like spatial Relation Algebra (RA) x, and is used to guide the change by imposing spatial constraints on objects of the "followed" spatial scene, eventually at different time points of the input trees. In order to capture the expressiveness of most modal temporal logics encountered in the literature, we introduce weakly cyclic Terminological Boxes (TBoxes) of MTALC(Dx), whose axioms capture the decreasing property of modal temporal operators. We show the important result that satisfiability of an MTALC(Dx) concept with respect to a weakly cyclic TBox can be reduced to the emptiness problem of a Buchi weak alternating automaton augmented with spatial constraints. In another work, complementary to this one, also submitted to this conference, we thoroughly investigate Buchi automata augmented with spatial constraints, and provide, in particular, a translation of an alternating into a nondeterministic, and an effective decision procedure for the emptiness problem of the latter.

Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to 'concrete' domains like numbers and strings with built-in predicates such as >, +, and prefix-of. These hybrid DLs have turned out to be useful in several application areas, such as reasoning about conceptual database models. We propose to further extend such DLs with key constraints that allow the expression of statements like 'US citizens are uniquely identified by their social security number'. Based on this idea, we introduce a number of natural description logics and perform a detailed analysis of their decidability and computational complexity. It turns out that naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.